A:Type, I:MaInterface(A), i:{i:Id| (i  fpf-domain(I))} . ((I(i).2).1)  (Knd List) 

latex

Definitions	Id, Type, a:A fp B(a), Knd, b, {x:A| B(x)} , State(ds), Top, left + right, x:AB(x), x:A  B(x), (x  l), f(x), t.2, t.1, t  T, type List, x:A. B(x), MaInterface(T), False, P  Q, A, P  Q, Dec(P), Atom$n, fpf-domain(f), f(a), hasloc(k;i), S  T, x. t(x), x.A(x), s = t
Lemmas	pi2 wf, pi1 wf, decl-state wf, l member wf, decidable l member, decidable equal Id